$\forall$$l_{1}$,$l_{2}$:IdLnk, $d_{1}$,$d_{2}$:fpf(Id; ${\it tg}$.Type).
\\[0ex](($l_{1}$ = $l_{2}$) $\Rightarrow$ fpf{-}compatible(Id; $x$.Type; id{-}deq; $d_{1}$; $d_{2}$))
\\[0ex]$\Rightarrow$ fpf{-}compatible(Knd; $x$.Type; Kind{-}deq; lnk{-}decl($l_{1}$; $d_{1}$); lnk{-}decl($l_{2}$; $d_{2}$))